Skip to content

Add Null & Boxed Types Support #143

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
rcosta358 wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Add Null & Boxed Types Support #143

rcosta358 wants to merge 4 commits into from

Conversation

@rcosta358
Copy link
Collaborator

@rcosta358 rcosta358 commented Feb 7, 2026 •
edited
Loading

This PR adds support for null checking in LiquidJava.
It also allows us to refine boxed types which previously were also not supported (Integer, Boolean, Short, Long, Float and Double).

Changes

Refinements Language

  • Added the null literal to the grammar
  • Added the LiteralNull AST node

Typing

  • The literal null can be assigned to any non-primitive type
  • String literals, literals of boxed types and new object instances implicitly carry the refinement _ != null, while the literal null carries the refinement _ == null

Z3 Translation

  • Nulls are converted to uninterpreted constants of the uninterpreted sort java.lang.Object
  • In equality comparisons, null literals are converted to the sort of the other operand to match both sorts
  • Boxed types are now mapped to the same Z3 sorts as their primitive types (e.g., java.lang.Integer => Int) to avoid errors like “Sorts java.lang.Integer and Int are incompatible"

Simplification

  • The simplifier removes redundant null checks when an equality to a non-null literal already implies a non-null value. This way, s == -1 && s != null simplifies to s == -1 instead of -1 != null

Testing

  • Added various tests to ensure the correctness of these changes

@rcosta358 rcosta358 self-assigned this Feb 7, 2026
@rcosta358 rcosta358 added the enhancement New feature or request label Feb 7, 2026
CatarinaGamboa
CatarinaGamboa requested changes Feb 9, 2026
View reviewed changes
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For the nullness check, I think we need more cases, like what if we declare the var and it doesn't have a value?
There are full tools just for the nullness checking (e.g., NullAway https://github.com/uber/NullAway)

PS: this would be so much easier if it were 2 prs, one for null and one for boxed types -- the boxed types would be an easy squash and merge

...va-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
if (refinementFound == null) {
refinementFound = new Predicate();
}
if (Utils.isBoxedType(localVariable.getType()) && !Utils.isNullLiteral(e)) {
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why is this necessary? and why wouldnt we put a createNullEq in the "only declaration, no assignment"?

Copy link
Collaborator Author

@rcosta358 rcosta358 Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  • That's the case where we declare a variable of boxed type (e.g. Integer) and it is not null, so it carries the refinement "_ != null"
  • I didn't consider uninitialized variables, should we handle that case?

@rcosta358
Copy link
Collaborator Author

rcosta358 commented Feb 9, 2026 •
edited
Loading

  • In Java if a variable is declared without a value it is not null, right? It's just not initialized. In those cases if one tried to use it it would be a Java error. Do we need to worry about that?
  • Fair point. I'll try to make more atomic PRs in the future!

rcosta358

This comment was marked as resolved.

Sign in to view

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@CatarinaGamboa CatarinaGamboa CatarinaGamboa requested changes

Requested changes must be addressed to merge this pull request.

Assignees

@rcosta358 rcosta358

Labels

enhancement New feature or request

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@rcosta358 @CatarinaGamboa